The sheer complexity of the software development process makes it increasingly difficult for programmers to detect programming flaws. As a result, software testing has become an important part of software development. For example, when writing concurrent programs, a programmer must consider every possible interleaving of events among various processes. Despite decades of research and engineering experience, few programmers succeed in writing robust concurrent programs. Large teams can sometimes manage the problem organizationally: a core set of experienced people design a concurrency model while every other developer is required to follow it. Such an approach has been successful only to a limited extent. Concurrency-related bugs still surface in stress tests. Such bugs are very hard to reproduce, debug, and correct. Because more and more programmers are writing concurrent programs, problems associated with concurrency are predicted to grow.
Currently, testing systems do not systematically consider concurrencies between two or more asynchronous processes. Consequently, subtle communication disconnects in concurrent processes may remain undiscovered.
One technique for developing and testing software is systematic state space exploration. However, in practice, software of any significant magnitude has such large numbers of states that it has been infeasible for any systematic approach to cover all the reachable states. Also, traditional state space explorers analyze the behavior of a program one thread at a time. Thus, errors due to interactions between threads cannot be directly detected using these tools. For example, errors that occur only if an interrupt service routine interleaves with a dispatch routine in a particular way can lie undetected in the program after several months of stress testing. Thus, conventional state space exploration is of limited use. There thus remains a need for improved software modeling techniques.